M:MsgA, x:Id. ma-init-const(M;x)   

latex

Definitions	t  T, IdDeq, Id, x:A. B(x), Type, Void, f(x)?z, Top, x.A(x), x. t(x), x:AB(x), S  T, , a:A fp B(a), suptype(S; T), P  Q, f(x), constant_function(f;A;B), x  dom(f), b, , z != f(x)  P(a;z), M.ds(x), ma-init-const(M;x), x:A  B(x), MsgA
Lemmas	msga wf, assert wf, fpf-dom wf, constant function wf, top wf, fpf-ap wf, fpf-trivial-subtype-top, rationals wf, fpf-cap wf, fpf-cap-void-subtype, Id wf, id-deq wf